Skip to content

WIP: Extract local MLfix as valid Java expressions via fixK helpers#12

Open
hiroshi-cl wants to merge 1 commit into
java_extractionfrom
feat/mlfix
Open

WIP: Extract local MLfix as valid Java expressions via fixK helpers#12
hiroshi-cl wants to merge 1 commit into
java_extractionfrom
feat/mlfix

Conversation

@hiroshi-cl

Copy link
Copy Markdown

MLfixに対応します

codexのメモ

1. 再帰を「メソッド自己参照」に押し付ける fixK ヘルパー

static <A1, R> R fix1(Function<Function<A1,R>, Function<A1,R>> gen, A1 a1) {
  return gen.apply(x1 -> fix1(gen, x1)).apply(a1);
}

ローカル fix を fix1(go -> 本体, 引数) というただのメソッド呼び出し式に変換します。再帰の結び目は fix1 が自分自身を呼ぶことで作るので、ご要望にあった懸念(初期化前参照・effectively-final)はそもそも発生しない構造になっています — セル配列も unchecked キャストも不要。ここが最大の設計判断です。

2. 型は Java のターゲット型推論に解かせる

MLfix ノードは Dfix と違って型注釈を持たないため、(Supplier)() -> {...} のような明示型が必要な IIFE 方式は不可能でした。ジェネリックメソッドなら引数型 A1..AK は実引数から、戻り型 R は式の置かれた位置のターゲット型から javac が推論してくれます。これを成立させるための付随修正が2つ:

fix を束縛する let は印字前にインライン化(let(fix0(...), go -> ...) はターゲット型が届かず Object に潰れるため)
コンストラクタに帰納型への upcast ((natlist) new Cons(...)) を付与(new Nil() だと型変数が Nil クラスに過特殊化されて再帰呼び出しが型エラーになるため)

3. 相互再帰は印字前に AST レベルで消す(Bekić 変換)

相互再帰用の fix2_1, fix2_2, ... のようなヘルパー爆発を避け、印字前に相互 MLfix を単一 fix の入れ子に書き換える unmutualize を追加。even/odd なら fix0(evenp -> ... fix1(oddp -> ..., m) ...) になります。プリンタは常に単一 fix だけ扱えばよく、コードが単純に保てます(代償はグループサイズに指数的な複製ですが、実用上 N=2〜3 なので許容)。

おまけとして、調査中に見つかった既存バグ2件(MLmagic と MLcase が適用引数を握り潰す)も修正済み。検証は単一(K=2)・相互(K=0/K=1、Bekić の両消去パス)のテストを新設し、抽出 → javac → 実行時アサーションまで全通過しています。

The Java backend printed local MLfix as a statement sequence
(var f = ...; ...; f.apply(args)), which is invalid in expression
positions (lambda bodies, let RHS, function arguments). Every other
MiniML construct already prints as an expression.

Encode a local fix applied to K arguments as a call to a generated
generic helper fixK(gen, a1, ..., aK) that ties recursion by method
self-reference, so no cell arrays, unchecked casts, definite-assignment
or effectively-final issues arise. Argument types ground A1..AK
bottom-up and R is grounded by the target type of the expression
position. Helpers are emitted on demand per arity next to the let
helper (fix0 for unapplied fixes implies fix1).

Mutual fixpoint groups are eliminated before printing by a Bekić
rewrite (unmutualize) into nested single fixes, using mlutil's
permut_rels and gen_subst (now exported).

Supporting changes needed for javac type inference:
- Inline let-bound fix heads into their use sites (a fixK call in the
  targetless let() argument position would infer Object).
- Upcast constructor expressions to their inductive interface,
  ((natlist) new Cons(...)), to avoid over-specialized inference such
  as A2 := Nil; skipped for custom inductives. Expected outputs
  regenerated accordingly.
- Fix MLmagic and MLcase dropping the application args accumulator.

Known limitations: fixK calls in positions without a target type infer
R = Object (e.g. a fix application result bound by let); helper names
fixN can collide with user identifiers (same caveat as let);
parameterized inductives get raw-type casts.

Tests: local_fix (single recursion, applied K=2 and reused let-bound
fix) and local_fix_mutual (mutual even/odd, K=0 elim-last and K=1
elim-first paths), each with a runtime driver.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant